%\newpage
\section{The Process Language}\label{sec:syn}
%\todo{I would not call this the \evol{} calculus: I would do the other way around, namely saying this is a pi-calculus
%with adaptable processes}
%
%\todo{Saying that we are presenting the process language and then presenting the type system is very strange.
%I realize Dezani does like this, but it doesn't make sense for them either}

%\paragraph{Syntax} 
We extend standard session-typed languages~\cite{DBLP:conf/esop/HondaVK98}
with \emph{located processes} and \emph{update actions}.
This allows us to explicitly represent adaptation mechanisms in models of structured communications.
As in~\cite{DBLP:conf/ppdp/GarraldaCD06}, 
our language 
is instrumented with some elements which support the static analysis.
In particular, we %consider
%annotated versions of the constructs defined in~\cite{BGPZFMOODS};
%as we will see, such annotations are key in statically ensuring consistent session behavior. Also,  namely 
annotate processes  with 
\emph{session types}---denoted $\rho_\qua$\,---and 
\emph{interfaces} (collections of session types)---denoted $\Delta$.
Both elements are introduced in Def.~\ref{d:types}.

Our syntax builds upon the following  
base sets: \emph{channels}, ranged over $c, d, \ldots$;
\emph{names}, ranged over $a, b, x, \ldots$;
\emph{locations}, ranged over $l, l', \ldots$;
\emph{labels}, ranged over $n, n', \ldots$;
\emph{constants} (integers, booleans, names), ranged over $k, k', \ldots$;
\emph{process variables}, ranged over $\mathsf{X}, \mathsf{X}', \ldots$;
\emph{recursion variables}, ranged over $Y, Y', \ldots$;
and \emph{integers}, ranged over $j,h,\ldots$.
We use $u, u'$ to denote names and channels.
Then, \emph{processes}, ranged over $P, Q, R, \ldots$
and \emph{expressions}, ranged over $e, e', \ldots$
are given by the grammar in Table \ref{tab:syntax}.
%\todo{the idea is to send expressions, rather than values, assuming that $e \downarrow k$, i.e, 
%that expressions evaluate to constants. Still to add: expressions in the syntax, polyadicity.
%This is following~\cite{DBLP:conf/esop/HondaVK98}}
%We now give the syntax of processes. Some of the constructs are annotated with typing information; this is useful to ensure properties by static analysis.

%We propose here a variant of the \evol{} calculus \cite{BGPZFMOODS} that on top of the constructs that handle dynamic updates adds operators and annotations that are meant to implement safe sessions. 
%More precisely, the \evol{} language is based on the classical CCS constructs: input/output operators, parallel composition, recursion. To this first set of basic operators we add the ability of modeling systems that can dynamically update: thus adding locations and a special operator to update the content of locations. Finally we add a group of operators that implement sessions. 





%\begin{definition}[Syntax]\label{d:syntax}
%Processes are defined by the grammar in Table \ref{tab:syntax}.
%\begin{table*}[ht]
%$$
%\begin{array}{lclr}
%P & ::=  
%  	& c(x{:}\capab).P \sepr \outC{c}{v}.P & \text{Input/Output}\\
%  	& \sepr & \ifte{x=v}{P}{P} & \text{Conditional}\\
%  	& \sepr & P \parallel P \sepr \rec{X{:}\type{\Phi}{\Delta}}{P_X}& \text{Parallel, Recursion}\\	 
%	&\sepr& \component{l}{h}{\Delta}{P} ~~(h \geq 0) ~\sepr \updated{l}{X}{\Delta}{\Delta'}{U} & \text{Adaptable Process, Update Process}\\
%	&\sepr& \open{c:\rho}.P \sepr \close{c}.P & \text{Open/Close Session}	\\
%	&\sepr& \branch{c}{n:P \dots n:P} \sepr \select{c}{n}.P ~~~& \text{Branch and Select}\\
%	&\sepr& \restr{c}{P}  & \text{Channel hiding}	\\
%U	&::= & P_{\mathsf{X}} &\text{Update}
%\end{array}
%$$
%\caption{Syntax of processes.} \label{tab:syntax}
%\end{table*}
\begin{table}[t]
$$
\begin{array}{lclr}
P \!\!& \!\!::=  
	& \!\!\! \nopen{a}{c:\rho_\qua}.P  & \text{open session}	\\
	& \sepr & \!\!\!\outC{c}{\tilde{e}}.P & \text{data output}\\
  	&\sepr &  \!\!\! \inC{c}{\tilde{x}}.P  & \text{data input}\\
	& \sepr & \!\!\!\throw{c}{d}.P & \text{channel output}\\
    &\sepr &  \!\!\!\catch{c}{d}.P  & \text{channel input}\\
	&\sepr& \!\!\!\component{l}{h}{\Delta}{P} ~~(h \geq 0)  & \text{adaptable process}\\
    & \sepr & \!\!\! \mathsf{X}& \text{process variable} \\
	&\sepr& \!\!\!\updated{l}{X}{\Delta_1}{\Delta_2}{P} & \text{update process}\\
  	& \sepr & \!\!\!\ifte{e}{P}{Q} & \text{conditional}\\
	    & \sepr & \!\!\! Y& \text{recursion variable}\\	 
	& \sepr & \!\!\! \rec{Y{:}\Phi{\cdot}\Delta}{P}& \text{recursion}\\	
  	& \sepr & \!\!\! P \parallel P & \text{parallel}\\	 
	&\sepr& \!\!\! \branch{c}{n_1:P_1, \ldots, n_k:P_k} & \text{branching}\\
	&\sepr& \!\!\! \select{c}{n}.P & \text{selection}\\
		&\sepr& \!\!\! \close{c}.P & \text{close session}	\\
			&\sepr& \!\!\! \restr{u}{P}  & \text{name/channel hiding}	\\
			&\sepr& \!\!\! \mathbf{0}  & \text{inaction} \\
e	&::= & \!\!\! k &\text{constants} \\
    & \sepr & \!\!\! e_1 + e_2 \sepr e_1 - e_2  \sepr \ldots & \text{operators}
\end{array} 
$$
%\vspace{-4mm}
\caption{Process Syntax} \label{tab:syntax}
\end{table}
%\end{definition}

%\todo{Look for a nice and concise definition of U}

%Some comments to the processes in Table~\ref{tab:syntax} are in order. % for denoting the hole in a context $P(\mathsf{X})$. 
%The former are  whereas the latter are written ; 
%for simplicity, we write $\mathcal{X}, \mathcal{X}', \ldots$ to refer to either kind.

%We write $P_{\mathsf{X}}$ to refer to processes with occurrences of variables, in such a way
%that each $\mathsf{X}$ is bound to a context $U$. 
%(Analogously for recursion variables, for which we write $P_X$.)
%Also, we assume that names $l, l', \ldots$---used to denote process locations---come from a set that is disjoint from the set containing 
%$c, c', \ldots$, which are typically used to denote 
%communication channels.


%\begin{table}[t]
%$$
%\begin{array}{ll}
%(P \parallel Q) \parallel R \equiv P \parallel (Q \parallel R)\\
%
%P \parallel Q \equiv Q \parallel P & P \parallel \nil \equiv P \\
%
%\restr{a}{P} \parallel Q \equiv \restr{a}{P \parallel Q}&
%\restr{a}{\nil} \equiv \nil\\
%\restr{a}{\restr{b}{P}} \equiv \restr{b}{\restr{a}{P}} & 
%\restr{a}{\component{l}{h}{\Delta}{P}} \equiv \component{l}{h}{\Delta}{\restr{a}{P}}
%\end{array}
%$$
%\caption{Structural congruence rules} \label{tab:congruence}
%\end{table}







We comment on the non-standard constructs in Table~\ref{tab:syntax}; 
intuitions and conventions for the other constructs are as in~\cite{DBLP:conf/esop/HondaVK98}.
Processes $\nopen{a}{c:\rho_\qua}$  and $\close{c}.P$ 
are 
used to 
establish and close a session on channel $c$, resp.
Once established, structured behavior on channels is possible.
The exchange of expressions 
(with the expected simultaneous substitution $\sub{\tilde{k}}{\tilde{x}}$)
is as usual; channel passing  
(delegation) is also supported.
Thus, our language combines dynamic reconfiguration via channel passing
with runtime adaptation via \emph{located} and \emph{update processes}, as we explain next.

%$\component{l}{h}{\Delta}{Q}$
A \emph{located process} $\component{l}{h}{\Delta}{Q}$ denotes a
process $Q$  deployed at location $l$.
Inside $l$, process $Q$ can evolve on its own and interact with external processes;
we use $l$ as a reference for a potential update actions (see below).
In $\component{l}{h}{\Delta}{Q}$, 
%while $\Delta$ describes the interface of $Q$, 
$h$ stands for the number of active sessions in $Q$: 
our operational semantics uses this information to ensure that locations enclosing active 
sessions are not interrupted by update actions (consistency).
% \todo{rimuoverei testo fra parentesi}(that is, an adaptable process can be updated only if $h=0$), 
We write $P(\mathsf{X})$ to denote a process $P$ with zero or more occurrences of process variable $\mathsf{X}$.
Also, 
we write $Q\subst{P}{\mathsf{X}}$ to denote 
the process $Q$ in which free occurrences of $\mathsf{X}$ are substituted with $P$. %---substitution for recursion variables is analogous.
Then, an \emph{update process} $\updated{l}{X}{\Delta_1}{\Delta_2}{P}$ represents a built-in adaptation mechanism, 
located at $l$.
%able to interact with a located process with abilities $\Delta$, so as to \emph{evolve} to 
%a process with abilities $\Delta'$.
In fact, as explained  below, 
if the interface of $Q$ and $\Delta_1$ are 
\emph{compatible} then 
processes $\component{l}{h}{\Delta_1}{Q}$ and $\updated{l}{X}{\Delta_1}{\Delta_2}{P}$
may interact so as to \emph{evolve} into $Q\subst{P}{\mathsf{X}}$. 
%an adaptable process $\component{l}{h}{\Delta}{P}$. As a result of such interaction, the current content 
%of the adaptable process 
%substitutes all occurrences of $\mathsf{X}$ in 
%(context) $U$, thus resulting in a process $U\subst{P}{\mathsf{X}}$ with abilities $\Delta'$.
Thus, 
intuitively,
process $\updated{l}{X}{\Delta_1}{\Delta_2}{Q}$ 
behaves as a function which 
expects a process with interface compatible with $\Delta_1$ and 
returns an adapted process with interface $\Delta_2$.

%in the adaptable process and the map $\Delta_1 \rightarrow \Delta_2$ in the update operator, instead, are used to enable only updates that comply with the map: i.e. an update can occur only if $\Delta = \Delta_1$ thus updating an adaptable processes with the expected capabilities.
% until it synchronizes with an update $\update{l}{X}{\Delta_1 \rightarrow \Delta_2}{U}$. The update replaces the adaptable process $\component{l}{h}{\Delta}{P}$ with the process $U$ where the variable $X$ is substituted with the current state $P$ of the adaptable process -- cfr. Rule $\rulename{r:Upd}$.

%More formally:




%\begin{table}[t]
%$$
%\begin{array}{rcl}
%(\bullet)^{*h}_{\otimes \Delta} & ::= & \bullet \\
%(C \parallel P)^{*h}_{\otimes \Delta} & ::= & C^{*h}_{\otimes \Delta} \parallel P \\
%(\component{l}{k}{\Delta'}{C})^{*h}_{\otimes \Delta} & ::= & \component{l}{{k*h}}{\Delta'\otimes \Delta}{C^{*h}_{\otimes \Delta}} \\
%(\restr{c}{C})^{*h}_{\otimes \Delta} & ::= & \restr{c}{C^{*h}_{\otimes \Delta}}
%\end{array}
%$$
%\caption{Context update. Above,  $*\in \{+,-\}$  and $ \otimes \in \{\addelta, \midelta \}$.} \label{tab:contextupdate}
%\end{table}


%We usually write $P(\mathsf{X})$ to denote the \emph{(process) context} $P$ with free occurrences of the process variable $\mathsf{X}$.

Binders for the language are as follows: 
channel $c$ is bound in $\nopen{a}{c:\rho_{\qua}}.P$ and
$\tilde{x}$ is bound in $\inC{c}{\tilde{x}}.P$ (variables $x_1, \ldots, x_n$ are all distinct). 
%Following~\cite{DBLP:conf/esop/HondaVK98}, given $P$, 
The set of free and bound channels  
and names of a process $P$---noted $\mathsf{fn}(P)$, $\mathsf{fc}(P)$, $\mathsf{bn}(P)$, and $\mathsf{bc}(P)$, resp.
is as expected. 
We define  $\mathsf{fu}(P) \triangleq \mathsf{fn}(P) \cup \mathsf{fc}(P)$.
The treatment of recursion variables is also as customary. 
As for process variables, we assume update processes bind process variables in it. 
In all cases, we rely on usual notions of $\alpha$-conversion (noted $\equiv_\alpha$) and (capture-avoiding) substitution.
We %assume all binders in $\mathsf{open}$ prefixes to be distinct, and 
work only with closed processes.


The semantics of our language is given by 
a \emph{reduction semantics},
denoted $P \pired P'$, the smallest relation on processes generated by the rules in Table~\ref{tab:semantics}.
It relies on  
an evaluation relation on expressions (noted $e \downarrow k$) and on
a structural congruence relation, %noted $\equiv$ and 
 defined as
% (Table~\ref{tab:congruence}). 
the smallest congruence generated by the following laws:
$$
\begin{array}{c}
(P \!\parallel\! Q) \!\parallel\! R \!\equiv\! P \!\parallel\! (Q \!\parallel\! R) \quad \restr{u}{\component{l}{h}{\Delta}{P}} \!\equiv\! \component{l}{h}{\Delta}{\restr{u}{P}} \quad P \!\parallel\! \nil \!\equiv\! P  \\ %\quad P \!\equiv\! Q \text{ if } P \!\equiv\!_\alpha Q \\
P \!\parallel\! Q \!\equiv\! Q \!\parallel\! P  \quad
\restr{u}{\nil} \!\equiv\! \nil \quad
\restr{u}{\restr{u'}{P}} \!\equiv\! \restr{u'}{\restr{u}{P}} \\
\restr{u}{P} \!\parallel\! Q \!\equiv\! \restr{u}{P \!\parallel\! Q} ~~\text{(if $u \not\in \mathsf{fu}(Q)$)}   \quad P \!\equiv\! Q \text{ if } P \!\equiv\!_\alpha Q
\end{array}
$$

\begin{table}[t]
$$
%\begin{array}{lr}
%\restr{c}{E\big[C[c(x:\capab).P] \parallel D[\outC{c}{v}.R]\big]} \pired & \\
%\quad \restr{c}{E\big[C[P\sub{v}{x}] \parallel D[R]\big]} \quad (\text{with } c \in \mathsf{fn}(E,D,C)) & \rulename{r:I/O} \vspace{1.5mm}
%\\
%C[\rec{X:\type{\Phi}{\Delta}}{P} ] \pired C[P\sub{\rec{X:\type{\Phi}{\Delta}}{P}}{X}] & \rulename{r:Rec} \vspace{1.5mm}
%\\
%C[\ifte{v=v}{P}{Q}] \pired C[P] & \rulename{r:IfTr} \vspace{1.5mm}
%\\
%C[\ifte{u=v}{P}{Q}] \pired C[Q]  \quad (\text{with } u \neq v)& \rulename{r:IfFa} \vspace{1.5mm}
%\\
%E\big[C[\component{l}{0}{\Delta_1}{P}] \parallel D[\updated{l}{X}{\Delta_1}{\Delta_2}{U}]\big] \pired  & \\
%\quad (E_{\midelta \Delta_1})_{\addelta \Delta_2}\big[(C_{\midelta \Delta_1})_{\addelta \Delta_2}[U\sub{P}{\mathsf{X}}] \parallel D[\nil]\big] & \rulename{r:Upd} \vspace{1.5mm}
%\\
%E\big[C[\open{c:\rho}.P] \parallel D[\open{d:\overline{\rho}}.R]\big] \pired  & \\
%\quad \restr{c'}{E^{+1}_{\midelta \{\rho, \overline{\rho}\}}\big[{C^{+1}_{\midelta \{\rho\}}[P\sub{c'}{c}] \parallel D^{+1}_{\midelta \{\overline{\rho}\}}[R\sub{c'}{d}]}\big]} \quad (\text{with $c'$ fresh}) & \rulename{r:Open} \vspace{1.5mm}
%\\
%\restr{c}{E\big[C[\close{c}.P] \parallel D[\close{c}.R]\big]} \pired & \\
%\quad \restr{c}{E^{-1}\big[C^{-1}[P] \parallel D^{-1}[R]\big]} & \rulename{r:Close} \vspace{1.5mm}
%\\
%\restr{c}{E\big[C[\branch{c}{n_i:P_i}_{i\in I}] \parallel D[\select{c}{n_j}.R]\big]} \pired  & \\
%\quad \restr{c}{E\big[C[P_j] \parallel D[R]\big]} & \rulename{r:Branch} \vspace{1.5mm}
%\\
%\text{if } P \equiv P',~ P' \pired Q', \text{ and } Q \equiv Q' ~~\text{then} ~~ P \pired Q & \rulename{r:Str}\vspace{1.5mm}
%\\
%\text{if } P \pired P' ~~\text{then} ~~ \restr{c}{P} \pired \restr{c}{P'} & \rulename{r:Res}
%\end{array}
%%%%%%
\begin{array}{l}
 \rulename{r:Open} \\ %~~ \text{Letting $\Delta_1 = \{c:\rho_{\qua}, \, d:\overline{\rho}_{\qua}\}, \Delta_2 = \{c:\rho_{\qua}\}, \Delta_3 \{d:\overline{\rho}_{\qua}\}$} \\
E\big[C[\nopen{a}{c:\rho_{\qua}}.P] \parallel D[\nopen{a}{d:\overline{\rho}_{\qua}}.Q]\big] \pired  
%~  \restr{c'}{\big(E^{+}_{\midelta \{c:\rho_{\qua}, \, d:\overline{\rho}_{\qua}\}}\big[{C^{+}_{\midelta \{c:\rho_{\qua}\} }[P\sub{c'}{c}] \parallel D^{+}_{\midelta \{d:\overline{\rho}_{\qua}\}}[Q\sub{c'}{d}]}\big]\big)} \vspace{1mm}
\\
\qquad  \qquad \qquad  \qquad \restr{c'}{\big(E^{+}_{}\big[{C^{+}_{}[P\sub{c'}{c}] \parallel D^{+}_{}[Q\sub{c'}{d}]}\big]\big)} 
 \vspace{1mm}
\\

\rulename{r:I/O} \\
E\big[C[\outC{c}{\tilde{e}}.P] \parallel D[\inC{c}{\tilde{x}}.Q]\big] \pired \\
\qquad \qquad \qquad  \qquad  \qquad \qquad E\big[C[P\sub{\tilde{k}}{\tilde{x}}] \parallel D[Q]\big] \quad (\tilde{e} \downarrow \tilde{k}) \vspace{1mm}
%\quad \qquad \qquad \qquad  \qquad \qquad  \qquad E\big[C[P\sub{v}{x}] \parallel D[Q]\big] %\vspace{1mm}
\\
\rulename{r:Upd} \\
E\big[C[\component{l}{0}{}{Q}] \parallel D[\updated{l}{X}{\Delta_1}{\Delta_2}{P}]\big]~~ 
(\text{with }\intf{Q} \compat\Delta_1)\pired   \\
\qquad\qquad  \qquad \qquad \qquad \qquad \qquad \qquad E_{}\big[C[P\sub{Q}{\mathsf{X}}] \parallel D[\nil]\big] \vspace{1mm}
\\
\rulename{r:Pass} \\
E\big[C[\throw{c}{d}.P] \parallel D[\catch{c}{d}.Q]\big] \pired E\big[C^{-}[P] \parallel D^{+}[Q]\big] \vspace{1mm}
\\
\rulename{r:Sel} \\
E\big[C[\branch{c}{n_i:P_i}_{i\in I}] \parallel D[\select{c}{n_j}.Q]\big] \pired \\
\qquad \qquad \quad \qquad \qquad \qquad \qquad \quad E\big[C[P_j] \parallel D[Q]\big]  \quad (j \in I)  \vspace{1mm}
% ~\quad\qquad \qquad \qquad E\big[C[P_j] \parallel D[Q]\big]  %\vspace{1mm}
\\
\rulename{r:Rec} \\
C[\rec{Y{:}\Phi{\cdot}\Delta}{P} ] \pired C[P\sub{\rec{Y{:}\Phi{\cdot}\Delta}{P}}{Y}]  \vspace{1mm}
\\
\rulename{r:IfTr} \\
C[\ifte{e}{P}{Q}] \pired C[P]  \quad (e \downarrow \mathtt{true})  \vspace{1mm}
\\
 \rulename{r:IfFa} \\
C[\ifte{e}{P}{Q}] \pired C[Q]  \quad (e \downarrow \mathtt{false}) \vspace{1mm}
\\
\rulename{r:Close} \\
E\big[C[\close{c}.P] \parallel D[\close{c}.Q]\big] \pired  E^{-}\big[C^{-}[P] \parallel D^{-}[Q]\big] \vspace{1mm}
%\qquad \qquad  \qquad \qquad  ~\qquad \qquad E^{-1}\big[C^{-1}[P] \parallel D^{-1}[Q]\big] %\vspace{1mm}
\\
 \rulename{r:Str} \\
\text{if } P \equiv P',\, P' \pired Q', \,\text{and}\, Q' \equiv Q ~\text{then} ~ P \pired Q \vspace{1mm}
\\
 \rulename{r:Res} \\
\text{if } P \pired P' ~~\text{then} ~~ \restr{u}{P} \pired \restr{u}{P'} %\vspace{2mm} \\
%\text{\emph{In \rulename{r:Open}, we assume $c'$ is fresh.}} \\
%\text{\emph{In \rulename{r:I/O}, we assume $c \in \mathsf{fn}(E,D,C)$.}}
\end{array}
$$  %\vspace{-4mm}
\caption{Reduction Semantics
%\emph{In $\text{\rulename{r:Sel}}$, $(j \in I)$.}
%\emph{In \rulename{r:I/O}, we assume $c \in \mathsf{fn}(E,D,C)$.}
}\label{tab:semantics}
\end{table}



%Reduction rules  require some additional definitions. 
We write $\pired^{*}$ for the reflexive, transitive closure of $\pired$.
%To represent the fact that 
As processes can be arbitrarily nested inside locations, 
in reduction rules we use  \emph{(syntactic) contexts}, i.e., processes with a \emph{hole} $\bullet$:
$$
C, D, E, \ldots ::= \bullet \sepr \component{l}{h}{\Delta}{C} \sepr C \parallel P   
$$
%\todo{toglierei for the sake of space} For the sake of space, w
We assume the expected extension of $\equiv$ 
%structural congruence 
to contexts.
To ensure coherence of located processes along reduction, 
 we define an operation over contexts
 which allows us
%Given $\component{l}{h}{\Delta}{P}$, they allow 
to increase/de\-crease $h$.
%the number of active sessions (given by $h$) 
%and to add/remove types from $\Delta$.
%abilities (given by $\Delta$).
%More precisely, g
Given a context $C$, an integer $j$,
and $* \in \{+,-\}$, %and $ \otimes \in \{\addelta, \midelta \}$, 
we define:
%operations $C^{*j}_{}$ and $C^{}_{\otimes \Delta}$
$$ (\bullet)^{*j}_{}  = \bullet \quad~~ (\component{l}{h}{\Delta}{C})^{*j}_{} = \component{l}{{h*j}}{\Delta}{C^{*j}_{}} \quad~~ (C \parallel P)^{*j}_{} = C^{*j}_{} \parallel P $$

%$$
%\begin{array}{rclcrcl}
%(\bullet)^{*j}_{} \!\!\!\!\!& ::= & \!\! \bullet \\ % & & (\bullet)^{}_{\otimes \Delta} \!\!\!\!\! & ::= & \!\! \bullet \\
%(\component{l}{h}{\Delta}{C})^{*j}_{} \!\!\!\!\! & ::= & \!\! \component{l}{{h*j}}{\Delta}{C^{*j}_{}} \\ %&  &  \!\! (\component{l}{h}{\Delta'}{C})^{}_{\otimes \Delta} \!\!\!\!\! & ::= & \!\! \component{l}{{h}}{\Delta'\otimes \Delta}{C^{}_{\otimes \Delta}}\\
%(C \parallel P)^{*j}_{} \!\!\!\!\! & ::= & \!\! C^{*j}_{} \parallel P % & & (C \parallel P)^{}_{\otimes \Delta} \!\!\!\!\! & ::= & \!\! C^{}_{\otimes \Delta} \parallel P
%%(\restr{c}{C})^{*j}_{} \!\!\!\!\! & ::= & \!\! \restr{c}{C^{*j}_{}} & & \!\!\!\!\!\!\!\!\! (\restr{c}{C})^{}_{\otimes \Delta} \!\!\!\!\! & ::= & \!\! \restr{c}{C^{}_{\otimes \Delta}}
%\end{array}
%$$
%\todo{
%\newcommand{\types}{\mathsf{type}}
%$$
%C_{\otimes \rho} = 
%\begin{cases}
%\bullet & \textbf{if } C= \bullet\\
%\component{l}{h}{\types(C, \rho)}{D_{\otimes \rho}}& \textbf{if } C= \component{l}{h}{\Delta}{D}\\
%D_{\otimes \rho} \parallel P& \textbf{if } C= D \parallel P
%\end{cases} 
%$$
%where $\types(C, \rho)$ is
%$$
%\types(C, \rho) = 
%\begin{cases}
%\rho & \textbf{if } C= \bullet\\
%l[\types(D,\rho)]& \textbf{if } C= \component{l}{h}{\Delta}{D}\\
%\types(D,\rho) + \quicktype(P) & \textbf{if } C= D \parallel P
%\end{cases} 
%$$
%By a slight abuse of notation,
We write ${C}^{-}$ and ${C}^{+}$ to stand for ${C}^{-1}$ and ${C}^{+1}$, resp.
We now comment on rules \rulename{r:Open}, \rulename{r:Close}, and \rulename{r:Upd} in Table~\ref{tab:semantics}; 
other rules are self-explanatory.


%Informally, 
%$\addelta$ (resp. $\midelta$)
%adds (resp. removes) session types from $\Delta$; a formal definition 
% is given in Sect.~\ref{s:types}.
%and write 
%${C}^{*k}_{\otimes \Delta}$ instead of $({C}^{*k})_{\otimes \Delta}$ and $({C}_{\otimes \Delta})^{*k}$.




Rule \rulename{r:Open} defines  session establishment by the interaction of two 
$\mathsf{open}$ prefixes on the same name and declaring \emph{dual session types} (cf. Def.~\ref{d:dual}).
When a session is initiated, the involved processes are restricted
with a channel $c'$, which we assume fresh. %, thus ensuring that channels are unique for each session. 
This way, channel restriction is only generated at runtime.
Because of session initiation, the number of active sessions 
is increased by one in 
%the located processes and propagated to 
all enclosing contexts.
%; also, the associated session should be removed from the interfaces of intervening processes. 
%This way, if the two interacting processes are inside a location, the annotations should be updated.
%Hence, in the rule we let 
%$\Delta_1 = \{c:\rho_{\qua}, \, d:\overline{\rho}_{\qua}\}, \Delta_2 = \{c:\rho_{\qua}\}, \Delta_3 \{d:\overline{\rho}_{\qua}\}$.
%These changes are realized with the above operations over contexts. 
%Notice that restriction is not used to build processes but only introduced by the semantics.
Rule \rulename{r:Close} is analogous:
it decreases the active session annotation in 
all enclosing contexts.
Let us write $\intf{P}$ for the \emph{interface} of process $P$ (cf. Sect.~\ref{s:types}). 
Rule \rulename{r:Upd} formalizes update actions. Two conditions are enforced: % which takes place if two conditions are met:
\begin{enumerate}[(1)]
\item Only 
located processes in which 
the number of open sessions is 0 can be updated.
This is to avoid disrupting already established sessions. %update actions which may interrupt session communications.
\item The interface of the located process ($\intf{Q}$) 
and the requirements of the update process ($\Delta_1$)
must be \emph{compatible}---noted $\Delta_1 \compat \intf{Q}$.
For the sake of simplicity, 
in the remainder we assume $\compat \, \triangleq \, = $.
Sect.\ref{sec:int} discusses more flexible  definitions.
%A simple (but too restrictive) definition is 
%requiring  both interfaces exactly match, i.e., letting $\compat \, \triangleq \, = $.
%%Alternative definitions are discussed later on. %We discuss more interesting forms later on.
%More appealing are notions of compatibility based on \emph{subtyping}~\cite{DBLP:journals/acta/GayH05,DBLP:journals/fuin/VallecilloVR06}.
%Although adding subtyping to our type structure (Sect.~\ref{s:types}) should not pose 
%any difficulties, the thorough treatment of notions of interface compatibility  
%is left for future work.
\end{enumerate}
An update (or evolvability) step  is then realized by 
  substituting $Q$ (the current behavior of the located process) into  $P(\mathsf{X})$.
% is updated and (ii) the annotations for the enclosing context must be adjusted so as to account for the moved interfaces. 
This is a form of \emph{objective update}, as the located process does not 
contain information on future update actions: it reduces autonomously until it is adapted by an  update process in its surrounding context. 



